home *** CD-ROM | disk | FTP | other *** search
/ Turnbull China Bikeride / Turnbull China Bikeride - Disc 1.iso / ARGONET / PD / PROGRAMMING / LCLINT2.SPK / test / test_a / db3 / lcl / ereftab < prev   
Text File  |  1996-08-28  |  624b  |  37 lines
  1. imports employee, eref;
  2.  
  3. mutable type ereftab; 
  4.  
  5. only ereftab ereftab_create(void) 
  6. {
  7.   /* ensures result' = empty; */
  8. }
  9.  
  10. void ereftab_insert(ereftab t, employee e, eref er) 
  11. {
  12.   /* requires getERef(t^, e) = erefNIL; */
  13.   modifies t;
  14.   /* ensures t' = add(t^, e, er); */
  15. }
  16.  
  17. bool ereftab_delete(ereftab t, eref er) 
  18. {
  19.   modifies t;
  20.   /* ensures result = in(t^, er) /\ t' = delete(t^, er); */
  21. }
  22.  
  23. eref ereftab_lookup(employee e, ereftab t) 
  24. {
  25.   /* ensures result = getERef(t^, e); */
  26. }
  27.  
  28. void ereftab_initMod (void) internalState;
  29. {
  30.   modifies internalState;
  31.   ensures true;
  32. }
  33.  
  34. iter ereftab_elements(ereftab s, yield eref x);
  35.  
  36.  
  37.